﻿using System;
using System.Diagnostics.Contracts;

namespace O1.Data.Traversal
{
    [ContractVerification(true)]
    public class EdgeSet
    {
        private EdgeMatch[] entries;

        private int[] buckets;

        private int count;

        public EdgeSet(int initialCapacity)
        {
            Contract.Requires<ArgumentOutOfRangeException>(0 < initialCapacity);
            Contract.Requires<ArgumentOutOfRangeException>(initialCapacity <= PrimeExtensions.MaxPrime);
                        
            Contract.Ensures(this.buckets != null);
            Contract.Ensures(this.buckets.Length > 0);
            Contract.Ensures(this.entries != null);
            Contract.Ensures(this.entries.Length > 0);
            Contract.Ensures(this.count == 0);
            Contract.Ensures(this.buckets.Length == this.entries.Length);

            var size = initialCapacity.RoundToPositivePrime();
            Contract.Assert(size >= 3);

            this.buckets = new int[size];
            for (int i = 0; i < this.buckets.Length; ++i)
            {
                this.buckets[i] = -1;
            }

            this.entries = new EdgeMatch[size];
            this.count = 0;
        }

        [CLSCompliant(false)]
        public bool Contains(EdgeDirections direction, ushort edgeType)
        {
            Contract.Ensures(this.buckets.Length == this.entries.Length);

            Contract.Assert(this.buckets != null);
            Contract.Assert(this.buckets.Length > 0);
            Contract.Assert(this.entries != null);
            Contract.Assert(this.entries.Length > 0);

            var targetBucket = edgeType % this.buckets.Length;
            Contract.Assert(targetBucket > -1);
            
            for (int i = this.buckets[targetBucket]; i >= 0; i = this.entries[i].Next)
            {
                Contract.Assume(i < this.entries.Length);
                if (this.entries[i].Direction.HasFlag(direction) && this.entries[i].EdgeType == edgeType)
                {
                    return true;
                }
            }

            return false;
        }

        [CLSCompliant(false)]
        public void Add(EdgeDirections direction, ushort edgeType)
        {
            Contract.Ensures(this.buckets != null);
            Contract.Ensures(this.buckets.Length > 0);
            Contract.Ensures(this.entries != null);
            Contract.Ensures(this.entries.Length > 0);
            Contract.Ensures(this.count > -1);
            Contract.Ensures(this.count <= this.entries.Length);

            Contract.Assert(this.buckets != null);
            Contract.Assert(this.buckets.Length > 0);
            Contract.Assert(this.entries != null);
            Contract.Assert(this.entries.Length > 0);
            Contract.Assert(this.count <= this.entries.Length);

            var bucket = edgeType % this.buckets.Length;
            Contract.Assert(bucket > -1);

            for (int i = this.buckets[bucket]; i >= 0; i = this.entries[i].Next)
            {
                Contract.Assume(i < this.entries.Length);
                if (this.entries[i].Direction.HasFlag(direction) && this.entries[i].EdgeType == edgeType)
                {
                   return;
                }
            }

            if (this.count == this.entries.Length)
            {
                Contract.Assume(this.count * 2 < PrimeExtensions.MaxPrime);
                var newSize = (this.count * 2).RoundToPositivePrime(2);
                var newBuckets = new int[newSize];
                for (int i = 0; i < newBuckets.Length; i++)
                {
                    newBuckets[i] = -1;
                }

                var newEntries = new EdgeMatch[newSize];
                Array.Copy(this.entries, 0, newEntries, 0, this.count);

                for (int i = 0; i < this.count; i++)
                {
                    bucket = newEntries[i].EdgeType % newSize;
                    newEntries[i].Next = newBuckets[bucket];
                    newBuckets[bucket] = i;
                }

                this.buckets = newBuckets;
                this.entries = newEntries;

                bucket = edgeType % this.buckets.Length;
            }

            Contract.Assume(this.count + 1 < this.entries.Length);

            var index = this.count;
            this.entries[index].Direction = direction;
            this.entries[index].EdgeType = edgeType;
            this.entries[index].Next = this.buckets[bucket];
            this.buckets[bucket] = index;
            this.count++;
        }

        [ContractInvariantMethod]
        [System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Performance", "CA1822:MarkMembersAsStatic", Justification = "Required for code contracts.")]
        private void ObjectInvariant()
        {
            Contract.Invariant(this.entries != null);
            Contract.Invariant(this.entries.Length > 0);
            Contract.Invariant(this.count >= 0);
            Contract.Invariant(this.count <= this.entries.Length);
            Contract.Invariant(this.buckets.Length == this.entries.Length);
        }

        private struct EdgeMatch
        {
            public int Next;

            public EdgeDirections Direction;

            public ushort EdgeType;
        }
    }
}
